feat(NumberTheory): non-vanishing derivative and algebraic lower bound for Gelfond-Schneider#35744
feat(NumberTheory): non-vanishing derivative and algebraic lower bound for Gelfond-Schneider#35744mkaratarakis wants to merge 12 commits intoleanprover-community:masterfrom
Conversation
PR summary 8f07524533
|
| Files | Import difference |
|---|---|
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlg (new file) |
2917 |
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlgSetup (new file) |
3127 |
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainOrder (new file) |
3133 |
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAnalytic (new file) |
3134 |
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainPostAnalytic (new file) |
3136 |
Declarations diff
+ A
+ IsIntegral.Cast
+ IsIntegral.Nat
+ IsIntegral_assoc
+ R
+ R_ne_zero
+ R_order
+ R_order_eq
+ R_order_prop
+ Rorder_exists
+ Setup
+ V
+ a
+ abs_crho_le_norm_crho
+ abs_q_pow_mul_house_le_c₃_pow
+ alpha'_beta'_gamma'_ne_zero
+ alpha'_ne_one
+ alpha_gamma_pow_beta_ne_zero
+ b
+ b_sum_ne_zero
+ beta'_ne_zero
+ beta_ne_zero
+ bound_c₁β
+ c1rho_neq_0
+ c1ρ
+ c5nonneg
+ c_coeffs
+ c_coeffs0
+ c_coeffs_neq_zero
+ c_coeffspow_r
+ cexp_mul
+ coeffs_mulVec_A_eq
+ coeffs_mul_deriv_eq_zero
+ crho_le_abs_crho
+ cρ
+ cρ_ne_zero
+ c₀
+ c₀Coeff
+ c₀Coeff_ne_zero
+ c₁
+ c₁IsInt
+ c₁_ne_zero
+ c₁_pow_sub_one_mul_c₁_pow_mul_c₁_pow_eq
+ c₁α_ne_zero
+ c₁γ_ne_zero
+ c₂
+ c₃
+ c₃_pow
+ c₄
+ c₅
+ deriv_R_k_eval_at_l0'
+ eq5
+ eq5zero
+ eq_iff_finProdFinEquiv_symm_ext
+ exists_common_field_of_isAlgebraic
+ exists_int_smul_isIntegral
+ exists_min_analyticOrderAt
+ exists_nonzero_iteratedFDeriv
+ h
+ h1
+ hM_ne_zero
+ hbound_sigma
+ house_add_mul_le
+ house_bound_c₁α
+ house_eta_le_c₄_pow
+ house_geq_1
+ house_matrixA_le
+ isInt_β_bound
+ isInt_β_bound_low
+ isIntegral_c₁_pow_smul_add_smul_pow
+ isIntegral_c₁_pow_smul_pow
+ isIntegral_c₁_pow_smul_α'_pow
+ isIntegral_c₁_pow_smul_α'_pow'
+ isIntegral_c₁_pow_smul_γ'_pow
+ isIntegral_c₁_pow_smul_γ'_pow'
+ isIntegral_c₁α
+ isIntegral_c₁β
+ isIntegral_c₁γ
+ isNumberField_adjoin_of_isAlgebraic
+ iteratedDeriv_R
+ iteratedDeriv_R_eq_zero
+ iteratedkDeriv_R_eq_zero
+ k
+ l
+ log_α_ne_zero
+ l₀'
+ l₀_prop
+ m
+ m_mul_n_lt_q_mul_q
+ m_mul_n_pos
+ mul_div_sub_eq_one
+ mul_rpow_sub_one_div_two
+ n
+ n_le_r
+ norm_Algebra_norm_rho_nonzero
+ norm_crho_le_house_crho
+ norm_cρ_pos
+ one_le_abs_c₁
+ one_le_c1rho
+ one_le_c₁
+ one_le_c₂
+ one_le_c₃
+ one_le_house_c₁γ
+ one_le_m
+ one_le_n
+ one_le_norm_c1rho
+ order_geq_n
+ order_geq_n_foo
+ order_neq_top
+ order_neq_top_min_one
+ q_eq_n_etc
+ q_le_two_mn
+ q_sq_eq_two_mn
+ q_sq_le_two_mn
+ r
+ r'
+ r'_spec
+ r_div_q_geq_0
+ r_exists
+ r_ne_zero
+ r_prop
+ r_spec
+ rho
+ rho_eq_ρᵣ
+ rho_injective
+ rho_nonzero
+ systemCoeffs
+ systemCoeffs_deriv
+ systemCoeffs_deriv_r
+ systemCoeffs_map_eq_exp_mul
+ systemCoeffs_map_eq_exp_mul_r
+ systemCoeffs_ne_zero_r
+ systemCoeffs_r
+ vandermonde_det_ne_zero
+ vecMul_V_eq_zero
+ zero_le_c1rho
+ zsmul_mul_mul_distrib
+ β'_ne_zero
+ η
+ ηvec_eq_zero
+ ρ
+ ρ_is_int
+ ρᵣ
+ ρᵣ_nonzero
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for scripts/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
Bot
added
the
t-number-theory
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
1 participant
This PR continues the formalization of the Gelfond-Schneider Theorem (Hilbert's Seventh Problem). It establishes the critical algebraic lower bound for the auxiliary function's evaluation by isolating its first non-vanishing derivative and scaling it to a non-zero algebraic integer.
Following the contradiction argument in Loo-Keng Hua's Introduction to Number Theory (Chapter 17.9, Equation 5), we extract the minimal non-vanishing derivative order$r$ and prove the integrality of its scaled evaluation to establish a strict analytical lower bound.
cρ) clears all denominators, resulting in an algebraic integer strictly within